Nuprl Lemma : inheres_wf
0,22
postcript
pdf
T
:Type,
x
:
T
,
a
:Atom1. AtomFree(Type;
T
)
x
:
T
>>
a
Prop
latex
Definitions
x
:
A
.
B
(
x
)
,
P
Q
,
t
T
,
Prop
,
x
:
T
>>
a
,
x
:
A
.
B
(
x
)
Lemmas
bool
wf
,
assert
wf
,
matters
wf
,
atom-free
wf
origin
T:Type, x:T, a:Atom1. AtomFree(Type;T) 
x:T>>a 
Prop T:Type, x:T, a:Atom1. AtomFree(Type;T) x:T>>a Prop x:A. B(x) Q T
x:A. B(x)